#ifndef __LITERAL_H__
#define __LITERAL_H__

// The definition of literal is Borrowed from MiniSat v1.14.

//=================================================================================================
// Lifted booleans:

#define __LBOOL_TRUE_INT	(1)
#define __LBOOL_FALSE_INT	(-1)
#define __LBOOL_UNDEF_INT	(0)

class Lbool {
public:
    __host__ __device__
	Lbool() : _value(0) { }
    __host__ __device__
	Lbool(bool x) : _value((int)x*2-1) { }
    __host__ __device__
	int convert_to_int(void) const { return _value; }
    __host__ __device__
	bool operator == (const Lbool& other) const { return _value == other._value; }
    __host__ __device__
	bool operator != (const Lbool& other) const { return _value != other._value; }
    __host__ __device__
	Lbool operator ~ (void) const
	{
		if ( _value == 1 )
		{ return Lbool(false); }
		else if ( _value == -1 )
		{ return Lbool(true); }
		else
		{ return Lbool(); }
	}

private:
    int _value;
};

const Lbool __Lbool_True  = Lbool(true);
const Lbool __Lbool_False = Lbool(false);
const Lbool __Lbool_Undef = Lbool();

//=================================================================================================
// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
// so that they can be used as array indices.

#define __LIT_UNDEF_INDEX	(-2)
#define __LIT_ERROR_INDEX	(-1)

class Lit {
public:
    __host__ __device__
	Lit() : _x(2*(-1)) {}   // (lit_Undef)
	__host__ __device__
	explicit Lit(int var, bool sign = false) : _x((var+var) + (int)sign) {}
	__host__ __device__
	~Lit() {}

	__host__ __device__
	bool sign (void) const { return _x & 1; }
	__host__ __device__
	int var (void) const { return _x >> 1; }
	__host__ __device__
	int index (void) const { return _x; } // A "toInt" method that guarantees small, positive integers suitable for array indexing.
	__host__ __device__
	unsigned int hash() const { return (unsigned int)_x; }

	__host__ __device__
	Lbool true_var_ass(void)
	{
		if ( _x == __LIT_UNDEF_INDEX )
		{ return Lbool(); }

		if ( (bool)(_x & 1) == true ) // ~X
		{ return Lbool(false); }
		else 
		{ return Lbool(true); }
	}

	__host__ __device__
	Lbool false_var_ass(void)
	{
		if ( _x == __LIT_UNDEF_INDEX )
		{ return Lbool(); }

		if ( (bool)(_x & 1) == true ) // ~X
		{ return Lbool(true); }
		else
		{ return Lbool(false); }
	}

	__host__ __device__
	Lbool value( Lbool assignment )
	{
		if ( assignment.convert_to_int() == 0 )
		{ return Lbool(); }
		else if ( assignment.convert_to_int() == 1 )
		{ return ((bool)(_x & 1) == false) ? Lbool(true) : Lbool(false); }
		else
		{ return ((bool)(_x & 1) == true) ? Lbool(true) : Lbool(false); }
	}

	__host__ __device__
	Lit operator ~ () const { Lit q; q._x = _x ^ 1; return q; }
	__host__ __device__
	bool operator == ( const Lit& q ) const { return _x == q._x; }
	__host__ __device__
	bool operator != ( const Lit& q ) const { return _x != q._x; }
	__host__ __device__
	bool operator < ( const Lit& q ) const { return _x < q._x; }  // '<' guarantees that p, ~p are adjacent in the ordering.

	friend Lit convert_to_lit ( int i );
	friend Lit convert_to_unsign( Lit p );
	friend Lit convert_to_id ( Lit p, bool sgn );

private:
    int _x;
};

__host__ __device__ inline
Lit convert_to_lit ( int i )
{ Lit p; p._x = i; return p; }  // Inverse of 'index()'.

__host__ __device__ inline
Lit convert_to_unsign( Lit p )
{ Lit q; q._x = p._x & ~1; return q; }

__host__ __device__ inline
Lit convert_to_id ( Lit p, bool sgn )
{ Lit q; q._x = p._x ^ (int)sgn; return q; }

__host__ __device__ inline
int toDimacs( Lit p )
{ return p.sign() ? -p.var() - 1 : p.var() + 1; }

const Lit __lit_Undef(-1, false);  // }- Useful special constants.
const Lit __lit_Error(-1, true );  // }

#endif /* __LITERAL_H__ */
